es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }. e[e1,e2].False  (e2 <loc e1) 

latex

Definitions	e[e1,e2].P(e), False, (e <loc e'), t  T, x:A. B(x), Prop, P  Q, P  Q, b, A, loc(e), Id, E, x. t(x), P & Q, P  Q, ES, e  e' , P  Q, Dec(P), Trans x,y:T. E(x;y)
Lemmas	es-le-trans, es-le wf, decidable es-locl, es-le-self, es-le-not-locl, event system wf, alle-between2 wf, false wf, es-E wf, Id wf, es-loc wf, es-loc-pred, es-locl wf